Concerning the security problem of local and global attacks on the Integrity Report Protocol (IRP), the StatVerif syntax was extended by adding constructors and destructors associated with the integrity measurement. The security of the Platform Configuration Attestation (PCA) was analyzed and the local and global attacks were found, including tampering the platform configuration register or revising stored measurement log by running unauthorized commands. The abilities of attackers were modeled, and how attackers accumulated knowledge and tampered PCA protocol by using constructors and destructors was introduced. Finally, the existence of attacking sequence was proved theoretically when PCA does not satisfy the correspondence property; and several propositions that PCA can meet the local reliability and gloabal reliability were given, which were proved by the formal verification tool Proverif.

Instant messaging is fundamental to various mobile Internet applications; however, it is still an open problem to implement secure instant messaging in untrusted Internet environment. An approach for secure instant messaging of mobile intelligent terminal was presented, and a protocol for Trusted Session Key Agreement (TSKA) was designed and implemented. Theoretical analysis shows that the proposed TSKA can ensure the authenticity, freshness and confidentiality of the negotiated session key, even in the condition that both of the instant messaging server and the communication channel are not trusted. After TSKA, instant audio/video messages can be sent to the other side in a confidential and complete way. Experimental results in real Internet environment show that the proposed approach is efficient and secure, the session key can be negotiated within 1-2 seconds, and attackers cannot obtain any plaintext of instant messages.